(set-logic QF_UFLRA)
(set-info :source |CPAchecker with k-induction on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)


(declare-fun |main::__CPAchecker_TMP_2@3| () Real)
(declare-fun |__ADDRESS_OF_main::x| () Real)
(declare-fun |__ADDRESS_OF_main::__CPAchecker_TMP_0| () Real)
(declare-fun |__ADDRESS_OF_main::__CPAchecker_TMP_1| () Real)
(declare-fun |main::x@4| () Real)
(declare-fun |__ADDRESS_OF_main::y| () Real)
(declare-fun |main::y@4| () Real)
(declare-fun |main::__CPAchecker_TMP_1@3| () Real)
(declare-fun |main::x@3| () Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(declare-fun |main::__CPAchecker_TMP_0@3| () Real)
(declare-fun |main::z@4| () Real)
(declare-fun |__ADDRESS_OF_main::__CPAchecker_TMP_2| () Real)
(declare-fun |__VERIFIER_assert::cond@2| () Real)
(declare-fun |__ADDRESS_OF_main::z| () Real)
(declare-fun |main::z@3| () Real)
(declare-fun |main::y@3| () Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real |__ADDRESS_OF_main::x|)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Real |__ADDRESS_OF_main::y|)
(define-fun _12 () Real (__BASE_ADDRESS_OF__ _11))
(define-fun _13 () Bool (= _11 _12))
(define-fun _14 () Bool (and _10 _13))
(define-fun _15 () Real |__ADDRESS_OF_main::z|)
(define-fun _16 () Real (__BASE_ADDRESS_OF__ _15))
(define-fun _17 () Bool (= _15 _16))
(define-fun _18 () Bool (and _14 _17))
(define-fun _19 () Real |main::x@3|)
(define-fun _20 () Bool (= _19 _7))
(define-fun _21 () Bool (and _18 _20))
(define-fun _22 () Real |main::y@3|)
(define-fun _23 () Bool (= _22 _7))
(define-fun _24 () Bool (and _21 _23))
(define-fun _25 () Real |main::z@3|)
(define-fun _26 () Bool (= _25 _7))
(define-fun _27 () Bool (and _24 _26))
(define-fun _28 () Real |__ADDRESS_OF_main::__CPAchecker_TMP_0|)
(define-fun _29 () Real (__BASE_ADDRESS_OF__ _28))
(define-fun _30 () Bool (= _28 _29))
(define-fun _31 () Bool (and _27 _30))
(define-fun _32 () Real 1048576)
(define-fun _33 () Real |main::__CPAchecker_TMP_0@3|)
(define-fun _34 () Real (* 1048576 _33))
(define-fun _36 () Real |main::x@4|)
(define-fun _37 () Real (- 1))
(define-fun _38 () Real (* (- 1) _36))
(define-fun _39 () Real (+ _34 _38))
(define-fun _40 () Real (+ _19 _39))
(define-fun _41 () Bool (= _40 _7))
(define-fun _42 () Bool (and _31 _41))
(define-fun _43 () Real |__ADDRESS_OF_main::__CPAchecker_TMP_1|)
(define-fun _44 () Real (__BASE_ADDRESS_OF__ _43))
(define-fun _45 () Bool (= _43 _44))
(define-fun _46 () Bool (and _42 _45))
(define-fun _47 () Real 2097152)
(define-fun _48 () Real |main::__CPAchecker_TMP_1@3|)
(define-fun _49 () Real (* 2097152 _48))
(define-fun _51 () Real |main::y@4|)
(define-fun _52 () Real (* (- 1) _51))
(define-fun _53 () Real (+ _49 _52))
(define-fun _54 () Real (+ _22 _53))
(define-fun _55 () Bool (= _54 _7))
(define-fun _56 () Bool (and _46 _55))
(define-fun _57 () Real |__ADDRESS_OF_main::__CPAchecker_TMP_2|)
(define-fun _58 () Real (__BASE_ADDRESS_OF__ _57))
(define-fun _59 () Bool (= _57 _58))
(define-fun _60 () Bool (and _56 _59))
(define-fun _61 () Real 4194304)
(define-fun _62 () Real |main::__CPAchecker_TMP_2@3|)
(define-fun _63 () Real (* 4194304 _62))
(define-fun _65 () Real |main::z@4|)
(define-fun _66 () Real (* (- 1) _65))
(define-fun _67 () Real (+ _63 _66))
(define-fun _68 () Real (+ _25 _67))
(define-fun _69 () Bool (= _68 _7))
(define-fun _70 () Bool (and _60 _69))
(define-fun _71 () Real 4)
(define-fun _72 () Real (* 4 _36))
(define-fun _78 () Real (- 2))
(define-fun _79 () Real (* (- 2) _51))
(define-fun _80 () Real (+ _79 _65))
(define-fun _81 () Real (+ _72 _80))
(define-fun _82 () Bool (= _81 _32))
(define-fun _83 () Bool (not _82))
(define-fun _84 () Real 1)
(define-fun _85 () Real (ite _83 _84 _7))
(define-fun _86 () Real |__VERIFIER_assert::cond@2|)
(define-fun _87 () Bool (= _85 _86))
(define-fun _88 () Bool (and _70 _87))
(define-fun _89 () Bool (= _86 _7))
(define-fun _91 () Bool (and _88 _89))



(assert _91)
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
